Nuprl Lemma : null-map
11,40
postcript
pdf
f
:top,
L
:(top List). sqequal(null(map(
f
;
L
)); null(
L
))
latex
Definitions
t
T
,
Y
,
map(
f
;
as
)
,
null(
as
)
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
f:top, L:(top List). sqequal(null(map(f; L)); null(L)) f:top, L:(top List). sqequal(null(map(f; L)); null(L)) 
Tx:A. B(x)